$\forall$$A$:Type, $B$:($A$$\rightarrow$Type).
\\[0ex]($\forall$$a$, $b$:$A$. Dec($a$ $=$ $b$)) $\Rightarrow$ ($\forall$$a$:$A$, $u$, $v$:$B$($a$). Dec($u$ $=$ $v$)) $\Rightarrow$ ($\forall$$x$, $y$:($a$:$A$$\times$$B$($a$)). Dec($x$ $=$ $y$))